<html>
<head><meta charset="utf-8"><title>coinductive all the way · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html">coinductive all the way</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="167876273"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167876273" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167876273">(Jun 11 2019 at 18:24)</a>:</h4>
<p>Hey <span class="user-mention" data-user-id="131694">@scalexm</span> -- so I've been wondering about whether it would be possible to make <strong>all</strong> trait matching coinductive.</p>



<a name="167876281"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167876281" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167876281">(Jun 11 2019 at 18:24)</a>:</h4>
<p>The obvious complication here has to do with implied bounds.</p>



<a name="167876300"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167876300" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167876300">(Jun 11 2019 at 18:24)</a>:</h4>
<p>The motivation is two-fold:</p>
<ul>
<li>simplicity (the mix of inductive + coinductive is a pain)</li>
<li>so-called "perfect derive"</li>
</ul>



<a name="167876315"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167876315" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167876315">(Jun 11 2019 at 18:24)</a>:</h4>
<p>I think this might require us to prove "fully implemented" predicates each time we prove <code>T: Trait</code></p>



<a name="167876325"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167876325" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167876325">(Jun 11 2019 at 18:25)</a>:</h4>
<p>(which <em>definitely</em> means we need to rename it =)</p>



<a name="167880326"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167880326" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167880326">(Jun 11 2019 at 19:04)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> interesting</p>



<a name="167880377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/167880377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#167880377">(Jun 11 2019 at 19:05)</a>:</h4>
<p>I’ll think about it and try to see if we can make it work</p>



<a name="168148568"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168148568" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168148568">(Jun 14 2019 at 16:08)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> i feel like it could work if we keep the separate <code>FromEnv</code> / <code>FullyImplemented</code> setting</p>



<a name="168148639"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168148639" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168148639">(Jun 14 2019 at 16:09)</a>:</h4>
<p>And that we lower all bounds to <code>FullyImplemented</code>:</p>
<div class="codehilite"><pre><span></span><span class="k">impl</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="k">where</span><span class="w"> </span><span class="n">T</span>: <span class="nc">Bar</span><span class="w"> </span><span class="p">{}</span><span class="w"></span>

<span class="c1">// Declared(T: Foo) :- FullyImplemented(T: Bar)</span>
</pre></div>



<a name="168148735"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168148735" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168148735">(Jun 14 2019 at 16:10)</a>:</h4>
<p>(Both <code>Declared</code> and <code>FullyImplemented</code> would be co-inductive, as always <code>FullyImplemented</code> is just a carrier traits enabling us to enumerate all the super <code>Declared</code> bounds on a trait)</p>



<a name="168148882"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168148882" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168148882">(Jun 14 2019 at 16:12)</a>:</h4>
<p>However merging <code>FullyImplemented</code> and <code>FromEnv</code> (i.e. having « true » reverse rules) is definitely not possible, i gave an example some time ago in the « alternate implied bounds lowering » stream</p>



<a name="168149703"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168149703" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168149703">(Jun 14 2019 at 16:22)</a>:</h4>
<p>Best thing to do would be to prototype in chalk, also I’ll have to re-spend a lot of time to convince myself this new setting is sound :)</p>



<a name="168152329"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168152329" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168152329">(Jun 14 2019 at 16:55)</a>:</h4>
<p>before we do that</p>



<a name="168152337"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168152337" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168152337">(Jun 14 2019 at 16:55)</a>:</h4>
<p>I have to fix the soundness bug in today's coinductive handling</p>



<a name="168152353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168152353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168152353">(Jun 14 2019 at 16:55)</a>:</h4>
<p>=)</p>



<a name="168152376"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168152376" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168152376">(Jun 14 2019 at 16:55)</a>:</h4>
<blockquote>
<p>However merging <code>FullyImplemented</code> and <code>FromEnv</code> (i.e. having « true » reverse rules) is definitely not possible, i gave an example some time ago in the « alternate implied bounds lowering » stream</p>
</blockquote>
<p>yeah I figured that the from-env/fully-impl split was the key innovation that might make this possible</p>



<a name="168873602"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168873602" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168873602">(Jun 24 2019 at 18:30)</a>:</h4>
<blockquote>
<p>I have to fix the soundness bug in today's coinductive handling</p>
</blockquote>
<p>I guess this isn't really a blocker -- <span class="user-mention" data-user-id="131694">@scalexm</span> is this something you'd be curious to play with?</p>



<a name="168873661"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168873661" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168873661">(Jun 24 2019 at 18:31)</a>:</h4>
<p>Also, remind me, you proved the soundness of the current setup -- or sketched a proof -- or something like that, right? I was discussing the whole setup with <span class="user-mention" data-user-id="116010">@Aaron Turon</span> a few days back and made an assertion like this, but I want to be sure I'm correct. =)</p>



<a name="168874283"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168874283" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168874283">(Jun 24 2019 at 18:39)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yes i sketched a proof that the current setup was correct in the absence of implied bounds from types, although I believe they’re quite trivial to add</p>



<a name="168874387"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168874387" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168874387">(Jun 24 2019 at 18:40)</a>:</h4>
<p>But the proof is very simple, basically an induction on the minimal depth of  a proof tree</p>



<a name="168874437"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/168874437" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#168874437">(Jun 24 2019 at 18:41)</a>:</h4>
<p>About the « coinductive all the way » setup, I could try to give it a go yeah</p>



<a name="173838130"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/173838130" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Hill <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#173838130">(Aug 21 2019 at 22:40)</a>:</h4>
<p>I'm interested in working on lazy normalization</p>



<a name="173838140"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/173838140" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Hill <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#173838140">(Aug 21 2019 at 22:40)</a>:</h4>
<p>Is that blocked on further integration of chalk?</p>



<a name="173838166"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/173838166" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Hill <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#173838166">(Aug 21 2019 at 22:41)</a>:</h4>
<p>Or is it something that's reasonable to work on right now?</p>



<a name="173838286"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinductive%20all%20the%20way/near/173838286" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Hill <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinductive.20all.20the.20way.html#173838286">(Aug 21 2019 at 22:43)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> eddyb suggested I ask you about this</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>